(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 1))
(let ((e3 1))
(let ((e4 8))
(let ((e5 (* (- e3) v1)))
(let ((e6 (/ e3 (- e2))))
(let ((e7 (* v0 (- e4))))
(let ((e8 (>= e6 e6)))
(let ((e9 (<= e6 v0)))
(let ((e10 (distinct v0 e5)))
(let ((e11 (> e5 v1)))
(let ((e12 (distinct v1 e6)))
(let ((e13 (>= v0 v0)))
(let ((e14 (= e7 e5)))
(let ((e15 (ite e10 e6 v0)))
(let ((e16 (ite e8 e6 e6)))
(let ((e17 (ite e11 v1 e5)))
(let ((e18 (ite e12 e7 v0)))
(let ((e19 (ite e13 e16 e6)))
(let ((e20 (ite e9 e5 e7)))
(let ((e21 (ite e14 e5 e16)))
(let ((e22 (distinct e5 e20)))
(let ((e23 (<= e18 e18)))
(let ((e24 (= e16 e18)))
(let ((e25 (distinct e19 e21)))
(let ((e26 (> e17 e6)))
(let ((e27 (distinct e18 e20)))
(let ((e28 (<= e17 e17)))
(let ((e29 (>= e16 e18)))
(let ((e30 (distinct e16 e6)))
(let ((e31 (< v1 e16)))
(let ((e32 (distinct e17 v0)))
(let ((e33 (distinct e18 e21)))
(let ((e34 (>= e16 e17)))
(let ((e35 (= v1 e7)))
(let ((e36 (< e19 e15)))
(let ((e37 (ite e25 e11 e27)))
(let ((e38 (xor e29 e35)))
(let ((e39 (xor e38 e31)))
(let ((e40 (= e14 e14)))
(let ((e41 (= e12 e23)))
(let ((e42 (and e13 e40)))
(let ((e43 (and e22 e22)))
(let ((e44 (= e37 e41)))
(let ((e45 (not e39)))
(let ((e46 (=> e9 e43)))
(let ((e47 (not e42)))
(let ((e48 (xor e26 e8)))
(let ((e49 (= e34 e36)))
(let ((e50 (ite e48 e48 e45)))
(let ((e51 (= e28 e10)))
(let ((e52 (and e49 e32)))
(let ((e53 (= e51 e47)))
(let ((e54 (and e53 e33)))
(let ((e55 (ite e44 e24 e44)))
(let ((e56 (and e54 e50)))
(let ((e57 (or e46 e55)))
(let ((e58 (ite e57 e56 e30)))
(let ((e59 (and e52 e58)))
e59
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
